module example/ringElection
open util/ordering[Time]
open util/ordering[Process]

// 時間
sig Time {
}

// 処理
sig Process {
	succ: Process,
	toSend: Process -> Time, 
	elected: set Time
}

fact Ring {
	all p: Process | Process in p.^succ
}

pred init(t: Time) {
	all p: Process | p.toSend.t = p
}

pred step(t, t': Time, p: Process) {
	let from = p.toSend, to = p.succ.toSend |
		some id: from.t {
			from.t' = from.t - id
			to.t' = to.t + (id - p.succ.prevs)
		}
}

pred skip(t, t': Time, p: Process) {
	p.toSend.t = p.toSend.t'
}
